
@book{Baader:1998:TR:280474,
  author    = {Franz Baader and
               Tobias Nipkow},
  title     = {Term rewriting and all that},
  publisher = {Cambridge University Press},
  year      = {1998},
  isbn      = {978-0-521-45520-6},
  pages     = {I-XII, 1-301},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  address = {New York, NY, USA},
} 


@article{DBLP:journals/iandc/LynchV95,
  author    = {Nancy A. Lynch and
               Frits W. Vaandrager},
  title     = {Forward and Backward Simulations: {I.~Untimed} Systems},
  journal   = {Inf. Comput.},
  volume    = {121},
  number    = {2},
  year      = {1995},
  pages     = {214-233},
  ee        = {http://dx.doi.org/10.1006/inco.1995.1134},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/rta/Meseguer00,
  author    = {Jos{\'e} Meseguer},
  title     = {Rewriting Logic and {Maude}: Concepts and Applications},
  booktitle = {RTA},
  year      = {2000},
  pages     = {1-26},
  ee        = {http://dx.doi.org/10.1007/10721975_1},
  crossref  = {DBLP:conf/rta/2000},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/rta/2000,
  editor    = {Leo Bachmair},
  title     = {Rewriting Techniques and Applications, 11th International
               Conference, RTA 2000, Norwich, UK, July 10-12, 2000, Proceedings},
  booktitle = {RTA},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {1833},
  year      = {2000},
  isbn      = {3-540-67778-X},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@inproceedings{DBLP:conf/tacas/MouraB08,
  author    = {Leonardo Mendon\c{c}a de Moura and
               Nikolaj Bj{\o}rner},
  title     = {Z3: An Efficient {SMT} Solver},
  booktitle = {TACAS},
  year      = {2008},
  pages     = {337-340},
  ee        = {http://dx.doi.org/10.1007/978-3-540-78800-3_24},
  crossref  = {DBLP:conf/tacas/2008},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/tacas/2008,
  editor    = {C. R. Ramakrishnan and
               Jakob Rehof},
  title     = {Tools and Algorithms for the Construction and Analysis of
               Systems, 14th International Conference, TACAS 2008, Held
               as Part of the Joint European Conferences on Theory and
               Practice of Software, ETAPS 2008, Budapest, Hungary, March
               29-April 6, 2008. Proceedings},
  booktitle = {TACAS},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {4963},
  year      = {2008},
  isbn      = {978-3-540-78799-0},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/iandc/SerbanutaRM09,
  author    = {Traian-Florin {\c S}erb{\u a}nu{\c t}{\u a} and
               Grigore Ro{\c s}u and
               Jos{\'e} Meseguer},
  title     = {A rewriting logic approach to operational semantics},
  journal   = {Inf. Comput.},
  volume    = {207},
  number    = {2},
  year      = {2009},
  pages     = {305-340},
  ee        = {http://dx.doi.org/10.1016/j.ic.2008.03.026},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}



@article{DBLP:journals/entcs/EscobarMS09,
  author    = {Santiago Escobar and
               Jos{\'e} Meseguer and
               Ralf Sasse},
  title     = {Variant Narrowing and Equational Unification},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {238},
  number    = {3},
  year      = {2009},
  pages     = {103-119},
  ee        = {http://dx.doi.org/10.1016/j.entcs.2009.05.015},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/lisp/MeseguerT07,
  author    = {Jos{\'e} Meseguer and
               Prasanna Thati},
  title     = {Symbolic reachability analysis using narrowing and its application
               to verification of cryptographic protocols},
  journal   = {Higher-Order and Symbolic Computation},
  volume    = {20},
  number    = {1-2},
  year      = {2007},
  pages     = {123-160},
  ee        = {http://dx.doi.org/10.1007/s10990-007-9000-6},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@inproceedings{rosu-stefanescu-2012-oopsla,
  author    = {Grigore Ro{\c s}u and
               Andrei {\c S}tef{\u a}nescu},
  title     = {Checking reachability using matching logic},
  booktitle = {OOPSLA},
  year      = {2012},
  pages     = {555-574},
  ee        = {http://doi.acm.org/10.1145/2384616.2384656},
  crossref  = {DBLP:conf/oopsla/2012},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/oopsla/2012,
  editor    = {Gary T. Leavens and
               Matthew B. Dwyer},
  title     = {Proceedings of the 27th Annual {ACM SIGPLAN} Conference on
               Object-Oriented Programming, Systems, Languages, and Applications,
               {OOPSLA} 2012, part of {SPLASH} 2012, Tucson, AZ, USA, October
               21-25, 2012},
  booktitle = {OOPSLA},
  publisher = {ACM},
  year      = {2012},
  isbn      = {978-1-4503-1561-6},
  ee        = {http://dl.acm.org/citation.cfm?id=2384616},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@Misc{RL,
  author = 	 {Grigore Ro\c{s}u and Dorel Lucanu},
  title = 	 {Circular Behavioural Reasoning},
  howpublished = {Draft Document},
  OPTmonth = 	 {},
  OPTyear = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@inproceedings{rosu-stefanescu-2011-nier-icse,
title = {Matching {Logic}: {A} {New} {Program} {Verification} {Approach} ({NIER} {Track})},
author = {Grigore Ro\c{s}u and Andrei \c{S}tef\u{a}nescu},
booktitle = {ICSE'11: Proceedings of the 30th International Conference on Software Engineering},
year = {2011},
pages = {868--871},
ee = {http://doi.acm.org/10.1145/1985793.1985928},
doi = {doi:10.1145/1985793.1985928},
publisher = {ACM},
isbn = {978-1-4503-0445-0},
}

@inproceedings{CadarGKPSTV11,
  author    = {Cristian Cadar and
               Patrice Godefroid and
               Sarfraz Khurshid and
               Corina S. P{\u a}s{\u a}reanu and
               Koushik Sen and
               Nikolai Tillmann and
               Willem Visser},
  title     = {Symbolic execution for software testing in practice: preliminary
               assessment},
  editor    = {Richard N. Taylor and
               Harald Gall and
               Nenad Medvidovic},
  booktitle = {ICSE},
  year      = {2011},
  pages     = {1066-1071},
  publisher = {ACM},
  ee        = {http://doi.acm.org/10.1145/1985793.1985995}
}

@article{King76,
  author    = {James C. King},
  title     = {Symbolic Execution and Program Testing},
  journal   = {Commun. ACM},
  volume    = {19},
  number    = {7},
  year      = {1976},
  pages     = {385-394},
  ee        = {http://doi.acm.org/10.1145/360248.360252},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{Plotkin70,
  author = {Plotkin, Gordon D.},
  journal = {Machine Intelligence},
  pages = {153--163},
  title = {A Note on Inductive Generalization},
  volume = 5,
  year = 1970
}

@article{AlpuenteEMO09,
  author    = {Mar\'{\i}a Alpuente and
               Santiago Escobar and
               Jos{\'e} Meseguer and
               Pedro Ojeda},
  title     = {Order-Sorted Generalization},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {246},
  year      = {2009},
  pages     = {27-38},
  ee        = {http://dx.doi.org/10.1016/j.entcs.2009.07.013}
}


@article{DBLP:journals/cacm/King76,
  author    = {James C. King},
  title     = {Symbolic Execution and Program Testing},
  journal   = {Commun. ACM},
  volume    = {19},
  number    = {7},
  year      = {1976},
  pages     = {385-394},
  ee        = {http://doi.acm.org/10.1145/360248.360252},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/icse/CadarGKPSTV11,
  author    = {Cristian Cadar and
               Patrice Godefroid and
               Sarfraz Khurshid and
               Corina S. P{\u a}s{\u }areanu and
               Koushik Sen and
               Nikolai Tillmann and
               Willem Visser},
  title     = {Symbolic execution for software testing in practice: preliminary
               assessment},
  booktitle = {ICSE},
  year      = {2011},
  pages     = {1066-1071},
  ee        = {http://doi.acm.org/10.1145/1985793.1985995},
  crossref  = {DBLP:conf/icse/2011},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/icse/2011,
  editor    = {Richard N. Taylor and
               Harald Gall and
               Nenad Medvidovic},
  title     = {Proceedings of the 33rd International Conference on Software
               Engineering, ICSE 2011, Waikiki, Honolulu , HI, USA, May
               21-28, 2011},
  booktitle = {ICSE},
  publisher = {ACM},
  year      = {2011},
  isbn      = {978-1-4503-0445-0},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/sttt/PasareanuV09,
  author    = {Corina S. P{\u a}s{\u a}reanu and
               Willem Visser},
  title     = {A survey of new trends in symbolic execution for software
               testing and analysis},
  journal   = {STTT},
  volume    = {11},
  number    = {4},
  year      = {2009},
  pages     = {339-353},
  ee        = {http://dx.doi.org/10.1007/s10009-009-0118-1},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@inproceedings{DBLP:conf/kbse/PasareanuR10,
  author    = {Corina S. P{\u a}s{\u a}reanu and
               Neha Rungta},
  title     = {Symbolic PathFinder: symbolic execution of {Java} bytecode},
  booktitle = {ASE},
  year      = {2010},
  pages     = {179-180},
  ee        = {http://doi.acm.org/10.1145/1858996.1859035}
}

@inproceedings{DBLP:conf/issta/VisserPK04,
  author    = {Willem Visser and
               Corina S. P{\u a}s{\u a}reanu and
               Sarfraz Khurshid},
  title     = {Test input generation with {J}ava {PathFinder}},
  booktitle = {ISSTA},
  year      = {2004},
  pages     = {97-107},
  ee        = {http://doi.acm.org/10.1145/1007512.1007526},
  crossref  = {DBLP:conf/issta/2004},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/issta/2004,
  editor    = {George S. Avrunin and
               Gregg Rothermel},
  title     = {Proceedings of the {ACM/SIGSOFT} International Symposium on
               Software Testing and Analysis, {ISSTA} 2004, {B}oston, {M}assachusetts,
               {USA}, July 11-14, 2004},
  booktitle = {ISSTA},
  publisher = {ACM},
  year      = {2004},
  isbn      = {1-58113-820-2},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@proceedings{DBLP:conf/kbse/2010,
  editor    = {Charles Pecheur and
               Jamie Andrews and
               Elisabetta Di Nitto},
  title     = {ASE 2010, 25th IEEE/ACM International Conference on Automated
               Software Engineering,  Antwerp, Belgium, September 20-24,
               2010},
  booktitle = {ASE},
  publisher = {ACM},
  year      = {2010},
  isbn      = {978-1-4503-0116-9},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@MISC{pex,
   author  = {{Pex}: Automated exploratory testing for {.NET}},
   url         ={\texttt{http://research.microsoft.com/en-us/projects/pex}},
   note     ={\\ \texttt{http://research.microsoft.com/en-us/projects/pex}}
   }
   
 @inproceedings{HalleuxT08,
  author    = {Jonathan de Halleux and
               Nikolai Tillmann},
  title     = {Parameterized Unit Testing with {Pex}},
  booktitle = {TAP},
  year      = {2008},
  pages     = {171-181},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {4966},
  ee        = {http://dx.doi.org/10.1007/978-3-540-79124-9_12},
  }

   

@inproceedings{Godefroid:2005:DDA:1065010.1065036,
  author    = {Patrice Godefroid and
               Nils Klarlund and
               Koushik Sen},
  title     = {{DART}: directed automated random testing},
  booktitle = {PLDI},
  year      = {2005},
  pages     = {213-223},
  ee        = {http://doi.acm.org/10.1145/1065010.1065036},
  crossref  = {DBLP:conf/pldi/2005},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/pldi/2005,
  editor    = {Vivek Sarkar and
               Mary W. Hall},
  title     = {Proceedings of the {ACM SIGPLAN} 2005 Conference on Programming
               Language Design and Implementation, Chicago, IL, USA, June
               12-15, 2005},
  booktitle = {PLDI},
  publisher = {ACM},
  year      = {2005},
  isbn      = {1-59593-056-6},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@inproceedings{Sen:2005:CCU:1081706.1081750,
 author = {Sen, Koushik and Marinov, Darko and Agha, Gul},
 title = {{CUTE}: a concolic unit testing engine for {C}},
 booktitle = {Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering},
 series = {ESEC/FSE-13},
 year = {2005},
 isbn = {1-59593-014-0},
 location = {Lisbon, Portugal},
 pages = {263--272},
 numpages = {10},
 url = {http://doi.acm.org/10.1145/1081706.1081750},
 doi = {10.1145/1081706.1081750},
 acmid = {1081750},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {concolic testing, data structure testing, explicit path model-checking, random testing, testing {C} programs, unit testing},
}

@inproceedings{DBLP:conf/aplas/BerdineCO05,
  author    = {Josh Berdine and
               Cristiano Calcagno and
               Peter W. O'Hearn},
  title     = {Symbolic Execution with Separation Logic},
  booktitle = {APLAS},
  year      = {2005},
  pages     = {52-68},
  ee        = {http://dx.doi.org/10.1007/11575467_5},
  crossref  = {DBLP:conf/aplas/2005},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/aplas/2005,
  editor    = {Kwangkeun Yi},
  title     = {Programming Languages and Systems, Third Asian Symposium,
               APLAS 2005, Tsukuba, Japan, November 2-5, 2005, Proceedings},
  booktitle = {APLAS},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {3780},
  year      = {2005},
  isbn      = {3-540-29735-9},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@inproceedings{Cadar06exe:automatically,
  author    = {Cristian Cadar and
               Vijay Ganesh and
               Peter M. Pawlowski and
               David L. Dill and
               Dawson R. Engler},
  title     = {{EXE}: automatically generating inputs of death},
  booktitle = {ACM Conference on Computer and Communications Security},
  year      = {2006},
  pages     = {322-335},
  ee        = {http://doi.acm.org/10.1145/1180405.1180445},
  crossref  = {DBLP:conf/ccs/2006usa},
  bibsource = {DBLP, http://dblp.uni-trier.de},
}
@proceedings{DBLP:conf/ccs/2006usa,
  editor    = {Ari Juels and
               Rebecca N. Wright and
               Sabrina De Capitani di Vimercati},
  title     = {Proceedings of the 13th ACM Conference on Computer and Communications
               Security, CCS 2006, Alexandria, VA, USA, Ioctober 30 - November
               3, 2006},
  booktitle = {ACM Conference on Computer and Communications Security},
  publisher = {ACM},
  year      = {2006},
  bibsource = {DBLP, http://dblp.uni-trier.de},
}

@article{rosu-serbanuta-2010-jlap,
  title={An Overview of the {K} Semantic Framework},
  author={Grigore Ro{\c s}u and Traian Florin {\c S}erb{\u a}nu{\c t}{\u a} },
  journal={Journal of Logic and Algebraic Programming},
  volume={79},
  number={6},
  pages={397--434},
  year={2010},
  ee={http://dx.doi.org/10.1016/j.jlap.2010.03.012},
  doi={10.1016/j.jlap.2010.03.012},
}


@inproceedings{klover,
  author    = {Guodong Li and
               Indradeep Ghosh and
               Sreeranga P. Rajan},
  title     = {{KLOVER}: A Symbolic Execution and Automatic Test Generation
               Tool for {C++} Programs},
  booktitle = {CAV},
  year      = {2011},
  pages     = {609-615},
  ee        = {http://dx.doi.org/10.1007/978-3-642-22110-1_49},
  crossref  = {DBLP:conf/cav/2011},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/cav/2011,
  editor    = {Ganesh Gopalakrishnan and
               Shaz Qadeer},
  title     = {Computer Aided Verification - 23rd International Conference,
               CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings},
  booktitle = {CAV},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {6806},
  year      = {2011},
  isbn      = {978-3-642-22109-5},
  ee        = {http://dx.doi.org/10.1007/978-3-642-22110-1},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{Khurshid03generalizedsymbolic,
  author    = {Sarfraz Khurshid and
               Corina S. P{\u a}s{\u a}reanu and
               Willem Visser},
  title     = {Generalized Symbolic Execution for Model Checking and Testing},
  booktitle = {TACAS},
  year      = {2003},
  pages     = {553-568},
  ee        = {http://dx.doi.org/10.1007/3-540-36577-X_40},
  crossref  = {DBLP:conf/tacas/2003},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/tacas/2003,
  editor    = {Hubert Garavel and
               John Hatcliff},
  title     = {Tools and Algorithms for the Construction and Analysis of
               Systems, 9th International Conference, {TACAS} 2003, Held
               as Part of the Joint European Conferences on Theory and
               Practice of Software, {ETAPS} 2003, {Warsaw}, {Poland}, {April}
               7-11, 2003, Proceedings},
  booktitle = {TACAS},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {2619},
  year      = {2003},
  isbn      = {3-540-00898-5},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@article{Dillon:1990:VGS:78617.78622,
 author = {Dillon, Laura K.},
 title = {Verifying General Safety Properties of {Ada} Tasking Programs},
 journal = {IEEE Trans. Softw. Eng.},
 issue_date = {January 1990},
 volume = {16},
 number = {1},
 month = jan,
 year = {1990},
 issn = {0098-5589},
 pages = {51--63},
 numpages = {13},
 url = {http://dx.doi.org/10.1109/32.44363},
 doi = {10.1109/32.44363},
 acmid = {78622},
 publisher = {IEEE Press},
 address = {Piscataway, NJ, USA},
 keywords = {Ada, Ada tasking programs, automating partial correctness proofs, concurrent programs, deadlock, isolation approach, multiprocessing programs, mutual exclusion, program verification., safety properties verification, symbolic execution},
}


@inproceedings{Siegel:2006:UMC:1146238.1146256,
  author    = {Stephen F. Siegel and
               Anastasia Mironova and
               George S. Avrunin and
               Lori A. Clarke},
  title     = {Using model checking with symbolic execution to verify parallel
               numerical programs},
  booktitle = {ISSTA},
  year      = {2006},
  pages     = {157-168},
  ee        = {http://doi.acm.org/10.1145/1146238.1146256},
  crossref  = {DBLP:conf/issta/2006},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/issta/2006,
  editor    = {Lori L. Pollock and
               Mauro Pezz{\`e}},
  title     = {Proceedings of the {ACM/SIGSOFT} International Symposium on
               Software Testing and Analysis, {ISSTA} 2006, {Portland}, {Maine},
               {USA}, {J}uly 17-20, 2006},
  booktitle = {ISSTA},
  publisher = {ACM},
  year      = {2006},
  isbn      = {1-59593-263-1},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@inproceedings{Staats:2010:PSE:1831708.1831732,
  author    = {Matt Staats and
               Corina S. P{\u a}s{\u a}reanu},
  title     = {Parallel symbolic execution for structural test generation},
  booktitle = {ISSTA},
  year      = {2010},
  pages     = {183-194},
  ee        = {http://doi.acm.org/10.1145/1831708.1831732},
  crossref  = {DBLP:conf/issta/2010},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/issta/2010,
  editor    = {Paolo Tonella and
               Alessandro Orso},
  title     = {Proceedings of the Nineteenth International Symposium on
               Software Testing and Analysis, {ISSTA} 2010, {T}rento, {I}taly,
               {J}uly 12-16, 2010},
  booktitle = {ISSTA},
  publisher = {ACM},
  year      = {2010},
  isbn      = {978-1-60558-823-0},
  bibsource = {DBLP, http://dblp.uni-trier.de},
}


@inproceedings{Pasareanu04verificationof ,
  author    = {Corina S. P{\u a}s{\u a}reanu and
               Willem Visser},
  title     = {Verification of {J}ava Programs Using Symbolic Execution and
               Invariant Generation},
  booktitle = {SPIN},
  year      = {2004},
  pages     = {164-181},
  ee        = {http://dx.doi.org/10.1007/978-3-540-24732-6_13},
  crossref  = {DBLP:conf/spin/2004},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/spin/2004,
  editor    = {Susanne Graf and
               Laurent Mounier},
  title     = {Model Checking Software, 11th International {SPIN} Workshop,
               {Barcelona}, {Spain}, {April} 1-3, 2004, Proceedings},
  booktitle = {SPIN},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {2989},
  year      = {2004},
  isbn      = {3-540-21314-7},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}



@article{Lee2003523,
title = {Generating test sequences using symbolic execution for event-driven real-time systems},
journal = "Microprocessors and Microsystems",
volume = "27",
number = "10",
pages = "523 - 531",
year = "2003",
note = "",
issn = "0141-9331",
doi = "10.1016/S0141-9331(03)00102-9",
url = "http://www.sciencedirect.com/science/article/pii/S0141933103001029",
author = "Nam Hee Lee and Sung Deok Cha",
keywords = "Real-time system testing",
keywords = "Symbolic execution",
keywords = "Modechart"
}


@inproceedings{schmitt07,
  author    = {Peter H. Schmitt and
               Benjamin Wei{\ss}},
  title     = {Inferring Invariants by Symbolic Execution},
  booktitle = {VERIFY},
  year      = {2007},
  ee        = {http://ceur-ws.org/Vol-259/paper16.pdf},
  crossref  = {DBLP:conf/cade/2007verify},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/cade/2007verify,
  editor    = {Bernhard Beckert},
  title     = {Proceedings of 4th International Verification Workshop in
               connection with {CADE}-21, {B}remen, {G}ermany, July 15-16, 2007},
  booktitle = {VERIFY},
  publisher = {CEUR-WS.org},
  series    = {CEUR Workshop Proceedings},
  volume    = {259},
  year      = {2007},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@techreport{lucanu:hal-00744374,
    hal_id = {hal-00744374},
    url = {http://hal.inria.fr/hal-00744374},
    title = {Program Equivalence by Circular Reasoning},
    author = {Lucanu, Dorel and Rusu, Vlad},
    abstract = {We propose a deductive system for automatically proving the equivalence of programs written in deterministic languages that have a formal, term-rewriting based operational semantics. Symbolic programs (i.e., programs in which some statements or expressions are symbolic variables) can also be proved equivalent using the proposed approach. The deductive system is circular in nature and is proved sound and weakly complete; together, these results say that, when it terminates, our system correctly solves the program-equivalence problem as we state it. We show that the deductive system is suitable for proving equivalence both for terminating and non-terminating programs. We also report on a prototype implementation of the proposed system in the $\mathbb{K}$ framework},
    language = {Anglais},
    affiliation = {Department of Computer Science , DART - INRIA Lille - Nord Europe},
    pages = {26},
    type = {Rapport de recherche},
    institution = {INRIA},
    number = {RR-8116},
    year = {2012},
    month = Oct,
    pdf = {http://hal.inria.fr/hal-00744374/PDF/RR-8116.pdf},
}

@MISC{imponline,
   author = {Symbolic IMP},
   title={https://fmse.info.uaic.ro/tools/Symbolic-IMP/},
   url="https://fmse.info.uaic.ro/tools/Symbolic-IMP/",
   year="2012"
}
@MISC{imphoare,
   author = {Symbolic IMP},
   title={https://fmse.info.uaic.ro/tools/Symbolic-IMP/},
   url="https://fmse.info.uaic.ro/tools/Symbolic-IMP/",
   year="2012"
}
@MISC{impreachability,
   author = {Symbolic IMP},
   title={https://fmse.info.uaic.ro/tools/Symbolic-IMP/},
   url="https://fmse.info.uaic.ro/tools/Symbolic-IMP/",
   year="2012"
}

@article{DBLP:journals/cacm/Hoare69,
  author    = {C. A. R. Hoare},
  title     = {An Axiomatic Basis for Computer Programming},
  journal   = {Commun. ACM},
  volume    = {12},
  number    = {10},
  year      = {1969},
  pages     = {576-580},
  ee        = {http://doi.acm.org/10.1145/363235.363259},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{rosu-stefanescu-2012-fm,
  author    = {Grigore Rosu and Andrei Stefanescu},
  title     = {From Hoare Logic to Matching Logic Reachability},
  booktitle = {Proceedings of the 18th International Symposium on Formal Methods (FM'12)},
  year      = {2012},
  pages     = {387-402},
  series    = {Lecture Notes in Computer Science},
  volume    = {7436},
  publisher = {Springer},
}